#数楽 そうだ、そうだ。Haskellではx :: (型)のような書き方をしますが、これは数学ではx∈(集合)のような意味だと思っておけば、数学に慣れた人は分かりやすいと思う。直後に但し書きの説明を加えるwhereもあって、これも数学っぽい。

#数楽 数学の説明では変数や項が何を指し示す変数や項なのか明示しておかないと不安なケースが多いので、「x∈Zに3x∈Zに対応させる写像」のような書き方をよくします。こういう慣習があることを知っていれば、Haskellでの x::(型) という書き方も受け入れ易いかも。

#数楽 "∈(集合)"を略さない方がよい場合：⋂_{i∈I} A_i = { x | すべての i について x∈A_i }「すべての i について」は右辺を見ただけで変数 i が動く範囲が明確になるようにするために「すべての i∈I について」と書く方が好ましい。

#数楽 継続モナド話続き TX=R^R^X が継続モナドの定義。 函数φ:X→TY=R^R^Yに対して、函数φ^*:TX=R^R^X→TY=R^R^Yが自然に対応していることを理解したい。(X→R^R^Y)≃(X×R^Y→R)≃(R^Y→R^X)より、～続く

#数楽 続き～、函数φ:X→R^R^Yと函数φ':R^Y→R^Xは一対一に対応している。ゆえに函数f:R^X→Rに合成函数f○φ':R^Y→Rを対応させる函数φ^*=(○φ'):R^R^X→R^R^Yが対応します。f○φ'がHaskellでのf>>=φに対応。

#数楽 状態モナドTX=(X×S)^Sでは、函数φ:X→(Y×S)^Sと函数φ':X×S→Y×Sが自然に一対一に対応していることから、函数f:S→X×Sに合成函数φ'○f:S→Y×Sを対応させる函数φ^*=(φ'○):(X×S)^S→(Y×S)^Sが定まるのであった。類似に注意。

#数楽 テキストで入力するときに自明でくだらない誤りをよく犯すのは、図式で描けば間違えようがない話をテキストで入力するのはあほらしいという気持ちがどうしても現われてしまうから。他のもっとすっきり明瞭な方法で考えているのに、それを文字で入力するのはもどかしい。全然違うものに変わる。

#数楽 継続モナド話続き。次のような函数列を考える。X_1→X_2→…→X_nこのとき函数X_{i+1}→Rには函数X_i→X_{i+1}との合成によって函数X_i→Rが対応する。だから次の函数列が得られる。R^{X_1}←R^{X_2}←…←R^{X_n}続く

#数楽 続き。例えば、X_i={整数全体}=Zで X_i→X_{i+1}が整数をn-i倍する函数ならば、X_0→X_1→…→X_nは左から順番にn倍、n-1倍、…、1倍する函数になり、その合成はn!倍する函数になり、それを1で評価すると値n!が得られる。これは普通の話。続く

#数楽 続き。これをRの右肩に載せると函数の向きが逆転して、R^{X_0}←R^{X_1}←…←R^{X_n}が得られる。右から順番に1倍、2倍、…、n倍する函数との合成によって別の函数を作る操作になっている。その合成は函数f(x)を函数f(n! x)に対応させる函数になる。

#数楽 同様にして、R^R^{X_0}→R^R^{X_1}→…→R^R^{X_n}が得られる。これの合成は函数f_0∈R^{X_0}をφ(f_0)∈Rに対応させる函数φを函数f_n∈R^{X_n}をφ(x↦f_n(n!x))∈Rに対応させる函数に対応させる函数になる。続く

#数楽 続き。函数に値を対応させる函数を函数を値に対応させる函数に対応させる函数を扱っているので、かなりややこしいことを考えていることになるのですが、矢印を繋げた図式を描けばそう難しくありません。続く

#数楽 続き。φ∈R^R^{X_0}を函数f∈R^{X_n}=(X_n→R)を1∈X_n=Zで評価する函数f↦f(1)だとし、RもR=Zであるとし、f_n=id_Zだとすると、 φ(x↦f_n(n! x))=id_Z(n! 1)=n! となり、めでたくn!が得られます。

#数楽 函数達X_i→X_{i+1]を反変函手X↦R^Xで移すと矢線の向きが逆転し、X_i上のR値函数の世界に移る。さらにもう一度反変函手Y↦R^Yでうつすと矢線の向きは元に戻り、X_i上のR値函数からRでの値を得る函数の世界に移る。こうして得られたX↦R^R^Xが継続モナド。

#数楽 上の階乗の例ではX_i→X_{i+1}をn-i倍する函数としたが、X_{i-1}→X_iをi倍する函数とした方が自然だったかも。R^{X_i}のレベルでの矢線の向きで階乗を計算するための函数が構成され、X_iもしくはR^R^{X_i}のレベルで逆向きに計算が実行される。

#数楽 継続モナドは反変函手X↦R^Xを二回合成したものなのですが、継続渡しスタイルにおいて、リソースを消費しながら函数を構成する計算の向きとそうやって構成された函数を評価する計算の向きが逆向きになるのは「反変函手が使われているからだ」と解釈できるんですね。

#数楽 再度警告。モナドやら計算の周辺に関して私は完璧など素人なのでこのツイートが繋がる返答連鎖の内容はど素人による発言だとみなして読んで下さい。以上でしているような話をど素人でもすぐにわかるように懇切丁寧に易しく解説してある文献を探しても見つけられなかった。

#数楽 チョー専門外のモナドの話の続き。継続モナドの定義は自己随伴な反変函手X↦R^Xを二回合成したものであることは数学的に自明な話なのですが、「継続モナドと継続渡しスタイルの関係はどうなっているんだ？」という疑問に答えようとしなければこの雑談の価値は小さくなります。

#数楽 続き。継続渡しスタイルの継続モナドTX=R^R^Xを使った表現は、計算をナマの函数α:X←Yで行うのではなく、対応する函手Tα:TX←TYと適当なTYの元から定まるTXの要素(計算を実行する函数になる)で行うと考えることによって得られます。矢線の向きに注意。

#数楽 Haskellでの継続モナドと継続渡しスタイルの関係に関する最も易しい例(flatten_cps)を使った解説はリンク先の後半にあります。(前半は継続モナドを使わない継続渡しスタイルの解説)http://www.geocities.jp/m_hiroi/func/haskell38.html …

#数楽 記号の対応私のノート ⇄ flatten_cpsγ ⇄ callCCe ⇄ kg ⇄ 計算例ではidに特殊化されている

#数楽 注意：私のノートの前者と後者の例におけるx_0が同じである必要な全くないのですが、flatten_cpsの例ではどちらのx_0も同じ空なリストに対応しています。例外的な場合の結果を空なリスト以外の値にすれば２つのx_0が異なる例を作れます。

#数楽 ある程度進んだある種の話が書いてある数学の文献では、「対象を矢線で繋げた図」を頻繁に利用します。函数(写像、より一般には射)が大量に出て来るややこしい話を理解したいときには矢線を繋げた図式がほぼ必須の道具になります。

#数楽 個人的な意見ですが、Haskellの入門的解説で「可換図式」などの図式が多用されていないのは異常事態に見えて仕方がない。

#数楽 X↦R^Xのような自己随伴反変函手が、その二回合成が継続モナドになることによって、「非常に役に立っている」様子は非常に面白い。

#数楽 @wwarotaw 数学では何かに名前を付けることによって面白い定理を簡潔に述べることができるなら名前を付けることに価値が出ます。たとえば「多角形の外角の和は〇〇になる」の形の命題を考えて、その命題が成立するように「多角形」の定義を可能な限り拡張してみたらどうですか？

#数楽 @wwarotaw 何をどう呼ぶかを決めるのが先ではなく、数学の世界でどういうことを成り立っているかに合わせて用語法をうまく調節するという感じになります。数学は他人に教わっても理解できることはほんの少ししかないので、自力でがんばってみて下さい。

#数楽 線形写像は写像の特別な場合ですが、線形写像は写像の一般化でもありますよね。集合XからYへの写像fは集合Xを基底に持つベクトル空間V(X)から集合Yを基底に持つベクトル空間V(Y)への線形写像V(f)に拡張される。V(f)の形をしていない線形写像は写像の一般化。量子化。

#数楽 訂正。誤「集合Xから生成される自由モナドをList X=[X]と書くと」→正「集合Xから生成される自由モノイドをList X=[X]と書くと」。指が混乱してしまった。https://twitter.com/genkuroki/status/830669374847488001 …

#数楽 数学と無関係のネタ。ツイッターでモナドについて検索すると、ゼノブレイドの主人公シュルクが装備する大剣モナドの画像がたくさん出て来る。次はGoogleでの検索。https://www.google.co.jp/search?q=�%83�ナド+ゼノブレイド …

#数楽combinatorial game category Joyal を検索https://www.google.co.jp/search?q=combinatorial+game+category+Joyal …

#数楽 訂正誤「組合せゲームの同値類にアーベル群の構造が入る」正「組合せゲームの同値類全体のクラスにアーベル群の構造が入る」https://twitter.com/genkuroki/status/832787116149010433 …

#数楽 さらに付け足すと、組合せゲームのあいだにはゲーム的に自然に射が定義されて、組合せゲームの圏が得られます。この辺のことまで定番のネタになると面白いのですが、まだ、面白い具体的な話のネタが発掘されていない感じかも。

#数楽 メモCodensity Monad - Just $ A sandbox http://myuon-myon.hatenablog.com/entry/2014/11/03/183032 …【mがFunctorやMonadでなくとも, CodensityはFunctorおよびMonadになる】「Kan拡張」を函手以外にも適用する話。

#数楽 メモYoneda lemmaとOperational Monad - Just $ A sandbox http://myuon-myon.hatenablog.com/entry/2013/06/09/135407 …米田函手のアイデアで函手でないものから函手を作る話。函手が得られれば、その函手から生成される自由モナドも得られる。

#数楽 リンクメモ：自由モナドの話http://myuon-myon.hatenablog.com/entry/20121111/1352608035 …http://myuon-myon.hatenablog.com/entry/2013/01/18/012935 …

#数楽 集合Sから生成された自由モノイドはSの要素を並べたリスト全体の集合だとみなせます。それと同様に(ある条件を満たす)自己函手Sから生成された自由モナドを作ることができる。函手は単なる集合よりも圧倒的に複雑な構造を持ち得るので自由モナドは自由モノイドより圧倒的に多彩。

#数楽 CodensityモナドについてX↦R^S^X=((X→S)→R)は函手になり、X↦R^R^X=((X→R)→R)はモナドになるので、函手とは限らないA↦P(A)とA↦F(A)に対して、X↦F(A)^P(A)^Xは函手になり、X↦F(A)^F(A)^Xはモナドになる。

#数楽 続き。こういうのも役に立っているのか。 FとPが函手の場合に X↦F(A)^P(A)^X はKan拡張を米田函手経由で見直したものになっているんですね。http://myuon-myon.hatenablog.com/entry/2014/11/03/183032 …

#数楽 続き。圏Cの対象Xに対して、Y_X(A)=A^X=Hom_C(X,A)が米田函手。米田の補題は函手F:C→SetについてHom_{Set^C}(Y_X,F)≅F(X)θ↦θ_X(id_X)(f↦Ff(x))↤xが成立するということ。続く

#数楽 続き。米田の補題の証明は、圏Cでの射f:X→Aはg∈Hom_C(X,X)=Y_X(X)を自然にf◦g∈Hom_X(X,A)=Y_X(A)に対応させるが、g=id_Xにはf自身が対応することに注意すれば、その後は単純作業に過ぎない話になる(試行錯誤すれば納得できる)。続く

#数楽 続き。圏Cの対象Xを集合F(X)に対応させる操作Fが与えられているとき、Fが函手でなくても、圏Cのすべての対象Aについて、Φ(X)=Hom_{Set}(Hom_C(X,A),F(A))はΦはXに関する函手になる。こういう自明な話が役に立っているんですね。続く

#数楽 続き。(Haskellなどで)型Xに型F(X)を対応させる操作Fを函手にするためのコードが書かれていないとき、Fを自動的に函手にする操作があればコードを書く手間を減らせます。FからΦ(X)=(∀A, (X→A)→F(A))を作る操作はまさにそれ！米田函手のアイデア。続く

#数楽 続き。数学科卒業生などですでに数学を知っている人が米田函手やKan拡大のアイデアがプログラミングで役に立つという話を勉強するときには、それらの構成法が教科書的な範囲を超えた場合に適用されていることに注意した方がいいかもしれません。それらの構成法が函手以外に適用されている。

#数楽 続き。ぶっちゃけ、自明な話。続く

#数楽 続き。数学的には自明でつまらない話であっても人間がする仕事の手間を減らすために役に立つ道具は結構たくさんあるのだと思う。そしてそういう道具を見付けることには地道な創造性が必要な感じがする。こつこつ積み上げる仕事は実際にやってみないとどういう感じなのかわからない。続く

#数楽 続き。リンクメモFreerモナドとCoyonedaについてhttp://qiita.com/masaki_mori/items/afb9696cac2476f0981c …【当たり前のものに変な名前を付けるのをやめてほしい】

#数楽 続き。リンクメモFreeモナドまとめhttp://qiita.com/masaki_mori/items/0fe34a6bb1b285be172a …【あえて同じ記号を濫用してわかりづらくすると】感覚的なところに色々共感してしまった。

#数楽 続き～F_3(X)={x, (op x x'), (op (op x x') x''), (op x (op x' x'')), (op (op (op x x') x'') x'''), …, (op x (op x' (op x'' x''')))}…続く～

#数楽 続き～となり、F_0(X), F_1(X), F_2(X), …の極限(今の場合は和集合)は「集合Xの元たちに二項演算記号opを形式的に有限回施した式全体の集合」になります。これがモナドになっていることはほぼ明らかです。続く

#数楽 続き。「集合Xの元たちに二項演算記号opを形式的に有限回施した式全体の集合」をT(X)=F^*(X)と書くことにします。T=F^*がモナドであるとは、函数η:X→T(X)、( )^*:(X→T(X))→(T(X)→T(Y))が定まっていて、モナド則を満たしていること。続く

#数楽 続き。函数η:X→T(X)=X⊔F(T(X))は単なる包含写像として自然に定まります。函数f:X→T(Y)は、Xの元x(型Xの要素x)へのYの元f(x)の代入を実行する函数f^*:T(X)→T(Y)を定めます。これらによってT=F^*は自然にモナドになります。続く

#数楽 続き。たとえば、f(a)=(op x y), f(b)=(op y x), f(c)=z のときf^*((op a (op b c)))=(op (op x y) (op (op y x) z))) です。f^*はfの自然な拡張になっています。続く